COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	∀E KW S,P,W
C00004 ENDMK
C⊗;
∀E KW S,P,W;
∀E REFLEX S,W;
∀E KNOW S,NOT(P),W;
∀E NOT W,P;
ASSUME T(K(S,NOT(P)),W);
TAUT  ∀W1.(A(S,W,W1)⊃T(NOT(P),W1)) 3,5;
∀E ↑ W;
⊃E 2,↑;
⊃I 5⊃↑;
TAUT (T(P,W)∧T(KW(S,P),W))⊃T(K(S,P),W) 1,4,9;
∀I ↑ S P W;
∀E KNOW S,P,W;
ASSUME T(K(S,P),W);
TAUT ∀W1.(A(S,W,W1)⊃T(P,W1)) 12:13;
∀E ↑ W;
⊃E 2,↑;
⊃I 13⊃↑;
∀I ↑ S P W;
∀E FOOL FOOL,P,W;
∀E FOOL S,K(FOOL,P),W;
∀E 18 FOOL,K(S,K(FOOL,P)),W;
TAUT T(K(FOOL,P),W)⊃T(K(S,K(FOOL,P)),W) 19:21;
∀I ↑ S W P;
∀E KNOW S,K(FOOL,P),W;
ASSUME T(K(FOOL,P),W);
TAUT ∀W1.(A(S,W,W1)⊃T(K(FOOL,P),W1)) 22 24:25;
∀E ↑ W1;
⊃I ↑↑↑⊃↑;
TAUT (T(K(FOOL,P),W)∧A(S,W,W1))⊃T(K(FOOL,P),W1) 28;
∀I ↑ S P W W1;


LABEL KW1=11;
LABEL KNOWTRUE=18;
LABEL FOOLTRUE=23;
LABEL FOOLTRANS=30;